A, B:es_realizer{i:l}, P:(ES{i}{i'}).
R-Feasible{i:l}(A)  B ||-{i} es.P(es)  R-compat{i:l}(A; B)  A  B ||-{i} es.P(es) 

latex

Definitions	P & Q, True, x. t(x), t  T, x(s), P  Q, , x:A. B(x)
Lemmas	Rplus wf, R-implies-rule, R-true-rule, es realizer wf, R-Feasible wf, event system wf, R-realizes wf, R-compat wf, true wf, R-and-rule